COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE OPCONST + -(NATNUM,NATNUM)=NATNUM [R←500,L←550]
C00005 ENDMK
C⊗;
DECLARE OPCONST + -(NATNUM,NATNUM)=NATNUM [R←500,L←550];
DECLARE OPCONST * /(NATNUM,NATNUM)=NATNUM [R←600,L←650];
DECLARE OPCONST + -(NATNUM)=NATNUM [PRE];

DECLARE PREDCONST ≤ ≥ < > (NATNUM,NATNUM) [INF];

DECLARE PREDCONST | (NATNUM,NATNUM)[INF];

DECLARE INDVAR U V W X Y Z;

DECLARE INDVAR M M0 M1 M2 N N0 N1 N2 ε NATNUM;

DECLARE PREDPAR A 1;

DECLARE PREDCONST NATNUM 1;

DECLARE OPCONST SUCC 1;

DECLARE PREDCONST ε 2[INF];

DECLARE OPCONST   ∪ 2[R←455 L←450];

AXIOM EXT: ∀X Y.(X=Y ≡ ∀Z.(ZεX ≡ ZεY));;

AXIOM NULLSET: ∀X.(¬Xε0);;

AXIOM PAIR: ∀X Y W.(Wε{X,Y} ≡ W=X ∨ W=Y);;

AXIOM UNIT: ∀X.({X} = {X,X});;

AXIOM UNION: ∀X Y W.((W ε X∪Y) ≡ WεX ∨ WεY);;

AXIOM NATNUM: ∀X.(NATNUM(X) ≡ ∀Y Z.(YεX ∧ ZεX ⊃ Y=Z ∨ YεZ ∨ ZεY)
	∧ ∀Y Z.(YεX ∧ ZεY ⊃ ZεX));;

AXIOM SUCC: ∀N.(SUCC(N) = N ∪ {N});;

AXIOM INDUCTION: A(0) ∧ ∀N.(A(N) ⊃ A(SUCC(N))) ⊃ ∀N.A(N);;

AXIOM ADDONE:	SUCC(0)=1,
		SUCC(1)=2,
		SUCC(2)=3,
		SUCC(3)=4,
		SUCC(4)=5,
		SUCC(5)=6,
		SUCC(6)=7,
		SUCC(7)=8,
		SUCC(8)=9;;

DECLARE OPCONST PRED(NATNUM) = NATNUM;

AXIOM PRED:	∀N.(PRED(SUCC(N)) = N),
		∀N.(¬(N=0) ⊃ SUCC(PRED(N)) = N);;

AXIOM PLUS:	∀M.(M+0 = M),
		∀M N.(M + SUCC(N) = SUCC(M+N));;

AXIOM TIMES:	∀M.(M*0 = 0),
		∀M N.(M*SUCC(N)) = (M*N+M);;

AXIOM GREATEQ:	∀M N.(M ≥ N ≡ ∃N1.(M = N+N1));;
  
AXIOM GREATER:	∀M N.(M > N ≡ ¬(N ≥ M));;

AXIOM LESSEQ:	∀M N.(M ≤ N ≡ (N ≥ M));;

AXIOM LESSER:	∀M N.(M < N ≡ (N > M));;

AXIOM MINUS:	∀M.(M-0 = M),
		∀M.(M-M = 0),
		∀M N.(M ≥ N ⊃ SUCC(M)-N = SUCC(M-N));;

AXIOM DIVIDE:	∀M N.(M|N ≡ ∃M1.(N = M*M1));;

DECLARE PREDCONST PRIME 1;


AXIOM PRIME:	∀M.(PRIME(M) ≡ ¬(M=0)∧¬(M=1)∧∀N.(N|M ⊃ N=1 ∨ N=M));;